FDL - Nuprl Lemma : generated-thread-binrel-properties2

Nuprl Lemma : generated-thread-binrel-properties2

es:ES, P:(E

), R:(E

E

).
single-thread-generator{i:l}(es;P;R)

(

e, e':E. (R(e,e'))

(P(e) & P(e')))

(connex({e:E| P(e)} ;R^*)

c

(R^+|P <

>{E} x,y:E. (x < y)|P)

c

(R <

>{E} R^+!)

c

(

x, y, x', y':E. (R^+(x,y))

(R(y',y))

((R^*)(x,y')))

c

(

x, y, x', y':E. (R^+(x,y))

(R(x',x))

(R(y',y))

(R^+(x',y'))))

Definitions x. t(x), x,y. t(x;y), suptype(S; T), S T, P Q, P Q, R|P, E <>{T} E', A c B, t T, x(s), P & Q, P Q, , x:A. B(x), {T}, x(s1,s2), a [r] b

Lemmas rel star functionality wrt breqv, binrel ap functionality wrt breqv, implies functionality wrt iff, all functionality wrt iff, rel-immediate functionality wrt breqv, binrel eqv weakening, rel plus functionality wrt breqv, binrel eqv functionality wrt breqv, cand functionality wrt iff, binrel ap wf, rel-immediate wf, es-causl wf, ab binrel wf, rel plus wf, rel-restriction wf, binrel eqv wf, rel star wf, xxconnex wf, event system wf, single-thread-generator wf, es-E wf, generated-thread-binrel-properties